
%{
  open Ast
  open Format

  type error = Missing_procs | Too_much_procs

  exception Error of error * Ast.loc

  let print_error = function
  | Missing_procs -> eprintf "Some process definitions are missing"
  | Too_much_procs -> eprintf "Too much process definitions are missing"
      
      
  let mk_loc e l = { data = l; node = e }

  let curloc () = Parsing.symbol_start_pos (),Parsing.symbol_end_pos()
    
  let loc e =
    mk_loc e (Parsing.symbol_start_pos (),Parsing.symbol_end_pos())

  let loc_i i e =
    mk_loc e (Parsing.rhs_start_pos i, Parsing.rhs_end_pos i)

  let loc_dummy e =
    mk_loc e (Lexing.dummy_pos, Lexing.dummy_pos)
 
%}

/* standard token */

/* associativity */


%token EOF
%token ARRAY ELSE END ENDIF FOR IF RETURN WHILE AWAIT ASSERT TRUE FALSE
%token DOTDOT LONGARROW IMPLIES ASSIGN DOT COMMA SC LCB RCB CONST
%token TYPE CRITICAL VAR ATOMIC ENDATOM THEN TO DO DONE CURRENT
%token LSB RSB LP RP AND BARBAR BAR NOT QM COL EQ NEQ LEQ GEQ NOT
%token LT GT PLUS MINUS TIMES DIV MOD AMPAMP AMP FORALL_OTHER EXISTS_OTHER
%token PROCCNT DECR ISZERO NOTZERO NUMPROC PROCESS
%token PROC BOOL REAL INT PROCCNT

%right ASSIGN
%left BARBAR /* || */
%left AMPAMP     /* && */
%left EQ NEQ                   /* == != */
%left LEQ GEQ LT GT                   /* < <= > >= */
%left PLUS MINUS             /* + - */
%left STAR SLASH PERCENT     /* * / % */
%right ustar uminus uplus BANG AMPERSAND
%nonassoc FORALL_OTHER EXISTS_OTHER
%left LSB par_expr

%token<string> IDENT
%token<string> MIDENT
%token<string> STRING
%token<int32> INTCONST
%token<float> REALCONST


  
%start prog
%type <Ast.loc Ast.prog> prog

%%
/*************************************************************
 * The structure of this file is loosely a depth-first preorder
 * traversal of the tree of the grammar.
 */

/* The whole thing. */
prog:
| decls CURRENT ident stmts  { $1, [$3, $4] }
| decls NUMPROC INTCONST procdefs  {
  let decls, nbprocs, procdefs = $1, $3, $4 in
  if Int32.of_int (List.length procdefs) > nbprocs
  then (raise (Error (Too_much_procs, curloc())))
  else if Int32.of_int (List.length procdefs) < nbprocs 
  then (raise (Error (Missing_procs, curloc())));
  (decls, procdefs)
  }
;

procdefs:
| procdef procdefs { $1::$2 }
| /* epsilon */ { [] }
  
procdef:
| PROCESS ident COL stmts { $2, $4 };
  
decls:
| /* epsilon */ { [] }
| decl decls { $1 :: $2 }
;

stmts:
| /* epsilon */ { [] }
| stmt stmts { $1 :: $2 }
;

decl:
| TYPE ident { Dtype ($2, []) }
| TYPE ident COL EQ constructor { Dtype ($2, $5) }
| CONST ident COL typ { Dvar (VDconst ($2, $4)) }
| VAR ident COL typ { Dvar (VDglobal ($2, $4)) }
| ARRAY mident LSB typ RSB COL typ { Dvar (VDarray ($2, $4, $7)) }
;

typ:
| PROC { Tproc }
| BOOL { Tbool }
| REAL { Treal }
| PROCCNT { Tproccnt }
| INT { Tint }
| ident { Tident $1 }
;

constructor:
| mident { [$1] }
| constructor BAR mident { $3::$1 }
;

mident:
| MIDENT { loc $1 }
;

ident:
| IDENT { loc $1 }
;

stmt:
| AWAIT qterm { loc (Sawait ($2, None)) }
| AWAIT qterm THEN stmt { loc (Sawait ($2, (Some $4))) }
| ATOMIC stmts END { loc (Satomic $2) }
| IF qterm THEN stmts ENDIF { loc (Sifelse ($2, $4, [])) }
| IF qterm THEN stmts ELSE stmts ENDIF { loc (Sifelse ($2, $4, $6)) }
| ASSERT qterm { loc (Sassert $2) }
| CRITICAL { loc Scritical }
| WHILE qterm DO stmts DONE { loc (Swhile ($2, $4)) }
| leftval ASSIGN term { loc (Sassign ($1, $3)) }
;

ident_list:
| ident { [$1] }
| ident COMMA ident_list { $1::$3 }
;

constnum:
| LP constnum RP { $2 }
| INTCONST { loc (Cint $1)}
| REALCONST { loc (Creal $1)}
;
    
term:
| atomic_term { loc ( TMatom $1) }
| atomic_term PLUS constnum { loc (TMarith (Bplus, $1, $3)) }
| atomic_term MINUS constnum { loc (TMarith(Bminus, $1, $3)) }
;

leftval:
| LP leftval RP { $2 }
| mident LSB ident_list RSB { loc (LVaccess ($1, List.rev $3)) }
| ident { loc (LVident $1)}
;

atomic_term:
| leftval { loc (ATleftval $1) }
| constnum { loc (ATconstnum $1) }
| mident {loc (ATenum $1) }
| LP FALSE RP { loc (ATbool false) } 
| LP TRUE RP { loc (ATbool true) }
| FALSE { loc (ATbool false) } 
| TRUE { loc (ATbool true) }
; 

qterm:
| quantifier { loc $1 }
| LP quantifier RP { loc $2 }
| logic_term { loc (Qterm $1) }
;

quantifier:
| FORALL_OTHER ident DOT logic_term { Qquantifier(Qforall, $2, $4)  }
| EXISTS_OTHER ident DOT logic_term { Qquantifier(Qexists, $2, $4)  }
;

logic_term:
| term { loc (LTterm $1) }
| literal { loc (LTlit $1) }
| LP logic_term BARBAR logic_term RP { loc (LTop (Bor, $2, $4)) }
| LP logic_term AMPAMP logic_term RP { loc (LTop(Band, $2, $4)) }
| logic_term BARBAR logic_term { loc (LTop (Bor, $1, $3)) }
| logic_term AMPAMP logic_term { loc (LTop(Band, $1, $3)) }
;

literal: 
| LP literal RP { $2 } 
| term NEQ term { loc (Bne, $1, $3) }
| term EQ term { loc (Beq, $1, $3) }
| term GT term { loc (Bgt, $1, $3) }
| term LT term { loc (Blt, $1, $3) }
| term LEQ term { loc (Ble, $1, $3) }
| term GEQ term { loc (Bge, $1, $3) }
;






